package lambda

type Term interface {
	Reduce(env Environment) Term
	substitute(n uint64, with Term) Term
}

type Environment interface {
	CallFunction(code uint64, args []Primitive) Primitive
	CallPredicate(code uint64, args []Primitive) bool
}

func Abs(t Term) Term {
	return Abstraction{t}
}

func App(fun Term, arg Term) Term {
	return Application{fun, arg}
}

func Ref(n uint64) Term {
	return Reference(n)
}

func Prim(bytes []byte) Primitive {
	return Primitive(bytes)
}

func NativeApp(code uint64, args []Term) Term {
	return NativeApplication{code, args}
}

func NativeIf(code uint64, args []Term) Term {
	return NativeConditional{code, args}
}

type Abstraction struct {
	term Term
}

func (abs Abstraction) Reduce(env Environment) Term {
	panic("cannot reduce Abstraction")
}

func (abs Abstraction) substitute(n uint64, with Term) Term {
	abs.term = abs.term.substitute(n+1, with)
	return abs
}

type Application struct {
	fun Term
	arg Term
}

func (app Application) Reduce(env Environment) Term {
	abs, ok := app.fun.(Abstraction)

	if !ok {
		app.fun = app.fun.Reduce(env)
		return app
	}

	return abs.term.substitute(1, app.arg)
}

func (app Application) substitute(n uint64, with Term) Term {
	app.fun = app.fun.substitute(n, with)
	app.arg = app.arg.substitute(n, with)

	return app
}

type Reference uint64

func (ref Reference) Reduce(Environment) Term {
	panic("cannot reduce Reference")
}

func (ref Reference) substitute(n uint64, with Term) Term {
	if n == uint64(ref) {
		return with
	}

	return ref
}

type Primitive []byte

func (prim Primitive) Reduce(Environment) Term {
	panic("cannot reduce Primitive")
}

func (prim Primitive) substitute(n uint64, with Term) Term {
	return prim
}

type NativeApplication struct {
	code uint64
	args []Term
}

func (napp NativeApplication) Reduce(env Environment) Term {
	args := make([]Term, len(napp.args))
	copy(args, napp.args)
	napp.args = args

	reduced := make([]Primitive, len(napp.args))

	for i, a := range napp.args {
		if p, ok := a.(Primitive); ok {
			reduced[i] = p
		} else {
			napp.args[i] = a.Reduce(env)
			return napp
		}
	}

	return env.CallFunction(napp.code, reduced)
}

func (napp NativeApplication) substitute(n uint64, with Term) Term {
	args := make([]Term, len(napp.args))
	copy(args, napp.args)
	napp.args = args

	for i, a := range napp.args {
		napp.args[i] = a.substitute(n, with)
	}

	return napp
}

type NativeConditional struct {
	code uint64
	args []Term
}

func (ncond NativeConditional) Reduce(env Environment) Term {
	args := make([]Term, len(ncond.args))
	copy(args, ncond.args)
	ncond.args = args

	reduced := make([]Primitive, len(ncond.args))

	for i, a := range ncond.args {
		if p, ok := a.(Primitive); ok {
			reduced[i] = p
		} else {
			ncond.args[i] = a.Reduce(env)
			return ncond
		}
	}

	result := env.CallPredicate(ncond.code, reduced)

	if result {
		return Abs(Abs(Ref(2)))
	}

	return Abs(Abs(Ref(1)))
}

func (ncond NativeConditional) substitute(n uint64, with Term) Term {
	args := make([]Term, len(ncond.args))
	copy(args, ncond.args)
	ncond.args = args

	for i, a := range ncond.args {
		ncond.args[i] = a.substitute(n, with)
	}

	return ncond
}
